Nuprl Lemma : Q-Q-glued-self-image
11,40
postcript
pdf
es
:ES,
A
,
B
:Type,
Ia
:AbsInterface(
A
),
f
:(
A
B
),
Q
:(E
E
).
Q-R-glued(
es
;
B
; (
e
.
f
(
Ia
(
e
)));
Ia
;
Q
;
f
'
Ia
;
Q
)
latex
Definitions
t
T
,
E(
X
)
,
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
es-E-interface-image
,
es-is-interface
wf
,
assert
wf
,
subtype
rel
function
,
Q-Q-glues-to-self-image
origin
es:ES, A, B:Type, Ia:AbsInterface(A), f:(A
B), Q:(EE
).
e.f(Ia(e))); Ia; Q; f'Ia; Q) es:ES, A, B:Type, Ia:AbsInterface(A), f:(AB), Q:(EE).
e.f(Ia(e))); Ia; Q; f'Ia; Q) 
Tx:A. B(x)
Q